signature ASSERT_STRUCTS =
sig
end

signature ASSERT =
sig
  include ASSERT_STRUCTS


  (* store state *)
  datatype st
    = Rf (* register file *)
    | Hp (* heap *)
    (*update the address "exp1" of the store "st" to the value of "exp2"*)
    | Upd of st * exp * exp  (*Upd(st, exp1, exp2)*)
  (* integer exp *)
  and exp
    = IntNum of int (* integer *)
    | Addr of int (* address *)
    | Plus of exp * exp (* add *)
    | Minus of exp * exp (* sub *)
    | Times of exp * exp (* mul *)
    | Sel of st * exp (* get value from the offset "exp" in store "st" *)
    | Eax
    | Ebx
    | Ecx
    | Edx
    | Esi
    | Edi
    | Esp
    | Ebp
    | Zf
    | Sf

  datatype etype
    = Int
    | Label
    | Wild

  datatype prop 
    = True
    | Imply of prop * prop
    | Not of prop
    | And of prop * prop
    | Or of prop * prop
    | Gt of exp * exp
    | Ge of exp * exp
    | Lt of exp * exp
    | Le of exp * exp
    | Eq of exp * exp
    | Ne of exp * exp
    | Ex of (string * etype) * prop
    | InDom of exp * st

  type state = st * st

  type assert = state -> prop

  type fspec = {fname:string, prec:assert, postc:assert}

(*  type guard = state -> state -> prop *)

  type specenv = fspec list

  type spec = {lab: string, asst: (assert option)}
               
  fun getspec lab [] = (raise Fail ("Impossible! No such label:"^lab^"\n"); (SOME(fn st => Not(True)))) (*WIP should raise Fail*)
    | getspec lab (spec::specl) = 
      case spec
       of  {lab=l, asst=NONE} => if lab=l
                                 then NONE
                                 else getspec lab specl
         | {lab=l, asst=(SOME(a))} => if lab = l
                                      then (SOME(a))
                                      else getspec lab specl
      

end
